g:Group{i}, e:|g|, a:. -a x(*;e;~) e = ~(a x(*;e;~) e)  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, Mon, IGroup, Group{i}, i x(op;id;inv) e
Definitions	t  T, True, T, , i x(op;id;inv) e, ff, P  Q, P & Q, P  Q, tt, P  Q, x:A. B(x), if b then t else f fi , IMonoid, IGroup, Unit, , Mon, Group{i},
Lemmas	grp inv wf, true wf, squash wf, int op wf, assert of lt int, bnot of le int, eqff to assert, bnot wf, lt int wf, assert of le int, eqtt to assert, le wf, assert wf, iff transitivity, bool wf, le int wf, grp id wf, grp op wf, grp car wf, monoid p wf, nat op zero, inverse wf, grp inv id